COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE INDCONST T F ε Proposition
C00007 ENDMK
C⊗;
DECLARE INDCONST T F ε Proposition;
DECLARE INDVAR Q Q1 Q2 Q3 ε Proposition;
DECLARE OPCONST And(Proposition,Proposition) = Proposition [L←555,R←550];
DECLARE OPCONST Or(Proposition,Proposition) = Proposition [L←535,R←540];
DECLARE OPCONST Implies(Proposition,Proposition) = Proposition [L←515,R←520];
DECLARE OPCONST Equiv(Proposition,Proposition) = Proposition [L←505,R←510];
DECLARE OPCONST Not(Proposition) = Proposition [R←575];

DECLARE PREDCONST true(situation,Proposition);
DECLARE PREDCONST nec(Proposition);

DECLARE INDCONST Pat Joe Mike ε Personconcept;
DECLARE INDVAR P P1 P2 P3 ε Personconcept;

DECLARE INDCONST s0 ε situation;
DECLARE INDVAR s s1 s2 s3 ε situation;

DECLARE INDVAR X X1 X2 X3 Y Y1 Y2 Y3 ε Thingconcept;
DECLARE OPCONST Equal(Thingconcept,Thingconcept) = Proposition [L←600,R←605];
DECLARE OPCONST Telephone(Personconcept) = Thingconcept [R←610];

DECLARE OPCONST Know(Personconcept,Thingconcept) = Proposition;
DECLARE OPCONST K(Personconcept,Proposition) = Proposition;
DECLARE OPCONST Loves(Personconcept,Personconcept) = Proposition;
DECLARE OPCONST Want(Personconcept,Proposition) = Proposition;
DECLARE OPCONST Future(Proposition) = Proposition [R←595];

DECLARE INDVAR Z Z1 Z2 Z3 ε Actionconcept;
DECLARE OPCONST Tell1(Personconcept,Personconcept,Proposition) = Actionconcept;
DECLARE OPCONST Tell2(Personconcept,Personconcept,Thingconcept) = Actionconcept;
DECLARE OPCONST Can(Personconcept,Proposition) = Proposition;


AXIOM And:	∀s Q1 Q2.(true(s,Q1 And Q2) ≡ true(s,Q1) ∧ true(s,Q2)),
		∀Q1 Q2.(nec(Q1 And Q2) ≡ nec(Q1) ∧ nec(Q2));;

AXIOM Or:	∀s Q1 Q2.(true(s,Q1 Or Q2) ≡ true(s,Q1) ∨ true(s,Q2));;

AXIOM Implies:	∀s Q1 Q2.(true(s,Q1 Implies Q2) ≡ true(s,Q1) ⊃ true(s,Q2));;

AXIOM Equiv:	∀s Q1 Q2.(true(s,Q1 Equiv Q2) ≡ (true(s,Q1) ≡ true(s,Q2)));;

AXIOM Not:	∀s Q.(true(s,Not Q) ≡ ¬true(s,Q));;

AXIOM nec:	∀Q s.(nec(Q) ⊃ true(s,Q)),
		∀Q P.(nec(Q) ⊃ nec(K(P,Q)));;


AXIOM Want:	∀P Q1 Q2.nec(Want(P,Q1) And K(P,Q2 Implies Future Q1) Implies
			Want(P,Q2)),
		∀P Q. nec(Want(P,Q) Implies K(P,Want(P,Q)));;

AXIOM Loves:	∀P1 P2 Q.nec(Loves(P1,P2) And K(P1,Want(P2,Q)) Implies Want(P1,Q));;

AXIOM Tell:	∀P1 P2 Q.nec(Know(P1,Q) Implies Can(P1,Know(P2,X)));;

AXIOM Can:	∀P Q.nec(Want(P,Q) And Can(P,Q) Implies Future Q),
		∀P Q Q1.nec(Q And Can(P,Q1) Implies Can(P,Q And Q1));;


AXIOM K:	∀P Q.nec(K(P,Q) Implies Q);;

AXIOM s0:	true(s0,K(Joe,Know(Pat,Telephone Mike))),
		true(s0,K(Joe,Loves(Pat,Joe))),
		true(s0,Want(Joe,Know(Joe,Telephone Mike)));;


MARK FOO;